first step to integrate grobner to coqeal #70
Conversation
|
This is great! But I think we need some documentation as well in the README.md to advertise the fact that we have a Gröbner basis and Buchberger algorithm formalization. It may be easiest to do this in a followup PR once this one is merged - I can do that documentation PR if @proux01 is OK with it. |
|
@palmskog sure, feel free to open a separate documentation PR based on the current one, I'll rebase/merge it after the current one. |
|
@thery thanks for the submission. I'd like to take some time to review it reasonably carefully, so please don't expect anything before next week. |
theory/grobner.v
Outdated
| Definition plt p q : bool := | ||
| has (fun m2 => | ||
| [&& m2 \notin msupp p, | ||
| all (fun m1 => ((m1 < m2)%O || (m1 \in msupp q))) (msupp p) & | ||
| all (fun m1 => ((m1 <= m2)%O || (m1 \in msupp p))) (msupp q)]) | ||
| (msupp q). |
There was a problem hiding this comment.
If it's a lexicographic order, why not defining it as
Import Order.DefaultSeqLexiOrder.
Definition ple p q : bool := (sort >=%O (msupp p) <= sort >=%O (msupp q))%O.There was a problem hiding this comment.
I've used it but I am not sure it makes my life easier.
There was a problem hiding this comment.
I'm not expecting it to make life easier by itself, but it seems to me that some lemmas in grobner.v are just generic properties on lexicographic orders. If they are not in order.v they could be added first in ssrcomplents (and later backported). I would expect this to simplify proofs in grobner.v while providing more reusable material.
| Qed. | ||
|
|
||
| Lemma plt_msuppl (p q r : {mpoly R[n]}) : | ||
| perm_eq (msupp p) (msupp q) -> (p < r) = (q < r). |
There was a problem hiding this comment.
It's rather a question related to multinomials, but those perm_eq make me wonder whether msupp should not be defined as sort >=%O (dom p) or something like that?
There was a problem hiding this comment.
The problem is that there is many notion of orders in polynomial. There is no reason to fix one.
There was a problem hiding this comment.
Sure but not fixing any order means msupp currently has no canonical form, hence this kind of lemmas with perm_eq. Multinomials chose an order on monomials, I think it makes some sense to use it to make msupp canonical (as offered in math-comp/multinomials#66 ). Even if this order is somewhat arbitrary, it seems better than no order.
There was a problem hiding this comment.
maybe msupp should take an order as parameter?
There was a problem hiding this comment.
Maybe. Can I let you try that in multinomials? ( math-comp/multinomials#66 should be a good starting point)
There was a problem hiding this comment.
not very successful. It starts going wrong here.
Now that mlead is parametrized most theorems need extra properties on the order that I don't know
how to package.
There was a problem hiding this comment.
I don't have any good solution right now.
Best short term solution is probably to use a functor to put generic lemmas taking a module with the order properties as argument. This functor could then be instantiated to get the lemmas for any specific order.
A better solution would probably be to have order structures on relations (o : rel T) instead of just types (T), like Monoid in bigop, maybe something to discuss in a forthcoming MathComp meeting (maybe @pi8027 would have a better idea).
Adding the file grobner.v